import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Set;

public class Node {

	public Node left;
	public Node right;
	public Node parent;
	public static final int AND = 0;
	public static final int OR = 1;
	public static final int NOT = 2;
	public static final int IMPLIES = 3;
	public static final int BICOND = 4;
	public static final int EXIST = 5;
	public static final int FORALL = 6;
	public static final int PREDICATE = 7;
	public static final int VARIABLE = 8;
	public static final int DUMMY = 100;
	public boolean isNegated;
	int type;
	String name;
	ArrayList<String> args = new ArrayList<String>();
	// for standardizing apart
	static char lastVariable = 'y';
	// for skolemizing
	static int lastFunction = 1;
	static char lastConstant = 'c';
	static HashSet<String> vars = new HashSet<String>();

	public boolean isOperation() {
		return type <= FORALL;
	}

	public boolean isOperand() {
		return !isOperation();
	}

	public void negate() {
		isNegated = !isNegated;
	}

	public boolean isNegated() {
		return isNegated;
	}

	public Node() {

	}

	public Node(int type) {
		this.type = type;
	}

	public Node(int type, String name) {
		this.type = type;
		this.name = name;
	}

	public void addArg(String x) {
		args.add(x);
	}

	public void convertToCNF() {
		eliminateBiCond();
		System.out.println("eliminateBiCond\n" + this);
		eliminateImplies();
		System.out.println("eliminateImplies\n" + this);
		pushNegation(false);
		System.out.println("pushNegation\n" + this);

		standarizeApart();
		System.out.println("standarizeApart\n" + this);

		skolemize();
		System.out.println("skolemize\n" + this);

		removeForAll();
		System.out.println("removeForAll\n" + this);

		distributeOrOnAnd();
		System.out.println("distributeOrOnAnd\n" + this);

	}

	public String toString() {
		if (type == AND)
			return "(" + left + " AND " + right + ")";
		if (type == OR)
			return "(" + left + " OR " + right + ")";
		if (type == PREDICATE) {
			String res = isNegated ? "!" : "";
			res += name + "(";
			for (int i = 0; i < args.size(); i++) {
				res += args.get(i);
				// System.out.println("ARGS " + args.get(i));
			}
			res += ")";
			return res;
		}
		if (type == EXIST)
			return "Exist(" + left.name + ") [" + right + "]";
		if (type == FORALL)
			return "ALL(" + left.name + ") [" + right + " ]";
		if (type == NOT)
			return "!" + right;
		if (type == IMPLIES)
			return left + " => " + right;
		if (type == DUMMY)
			return right.toString();
		return "NO SUCH TYPE " + type;
	}

	public void distributeOrOnAnd() {
		if (right != null)
			right.distributeOrOnAnd();
		if (left != null)
			left.distributeOrOnAnd();
		if (type == OR) {
			if (right.type == AND) {
				Node e1 = new Node(OR);
				Node e2 = new Node(OR);
				e1.left = left.clone();
				e1.right = right.left.clone();
				e2.left = left.clone();
				e2.right = right.right = clone();
				type = AND;
				left = e1;
				right = e2;
				left.distributeOrOnAnd();
				right.distributeOrOnAnd();

			} else if (left.type == AND) {
				Node e1 = new Node(OR);
				Node e2 = new Node(OR);
				e1.right = right.clone();
				e1.left = left.right.clone();
				e2.right = right.clone();
				e2.left = left.left = clone();
				type = AND;
				left = e2;
				right = e1;
				left.distributeOrOnAnd();
				right.distributeOrOnAnd();
			}
		}
	}

	public void removeForAll() {
		if (type == FORALL) {
			// delete for all
			if (parent.left == this)
				parent.left = right;
			else
				parent.right = right;
			if (right != null)
				right.removeForAll();
		} else {
			if (right != null)
				right.removeForAll();
			if (left != null)
				left.removeForAll();
		}
	}

	public void skolemize() {
		ArrayList<String> forAlls = new ArrayList<String>();
		HashMap<String, String> map = new HashMap<String, String>();
		skolemize(forAlls, map);
	}

	public void skolemize(ArrayList<String> forAlls, HashMap<String, String> map) {
		if (type == FORALL)
			forAlls.add(left.name);
		if (type == EXIST) {
			String replacement = "(";
			for (int i = 0; i < forAlls.size(); i++) {
				replacement += forAlls.get(i);
				if (i != forAlls.size() - 1)
					replacement += ",";
				else
					replacement += ")";
			}
			// replace by constant
			if (forAlls.size() == 0) {
				lastConstant = (char) (lastConstant + 1);
				replacement = lastConstant + "";
			} else
				replacement = "f" + (lastFunction++) + replacement;
			map.put(left.name, replacement);
			// delete this exist node
			if (parent.type == DUMMY) {
				left = null;
				type = DUMMY;
			}
			if (parent.left == this) {
				parent.left = right;
				// System.out.println("left");
			} else if (parent.right == this) {
				parent.right = right;
				// System.out.println("right");
			}
		}
		// replace
		if (type == PREDICATE) {
			for (int i = 0; i < args.size(); i++) {

				if (map.containsKey(args.get(i))) {
					// replace
					String replacement = map.get(args.get(i));
					args.set(i, replacement);
				}

			}
		}
		if (right != null)
			right.skolemize(forAlls, map);
		if (left != null)
			left.skolemize(forAlls, map);

		// backtrack and remove added forAll variable
		if (type == FORALL)
			forAlls.remove(forAlls.size() - 1);
	}

	/**
	 * Eliminates <=> to => AND <=
	 */
	public void eliminateBiCond() {
		if (type == BICOND) {
			type = Node.AND;

			Node rightTree = clone();
			rightTree.type = IMPLIES;

			Node leftTree = clone();
			leftTree.type = IMPLIES;
			// Swap
			Node temp = leftTree.left;
			leftTree.left = leftTree.right;
			leftTree.right = temp;

			left = leftTree;
			right = rightTree;
		}
		if (left != null)
			left.eliminateBiCond();
		if (right != null)
			right.eliminateBiCond();
	}

	public void standarizeApart() {
		HashMap<String, String> map = new HashMap<String, String>();
		standarizeApart(map);
	}

	public void standarizeApart(HashMap<String, String> map) {
		if (type == PREDICATE) {
			for (int i = 0; i < args.size(); i++)
				if (map.containsKey(args.get(i)))
					args.set(i, map.get(args.get(i)));
			return;
		}
		if (type == EXIST || type == FORALL) {
			String var = left.name;
			String previous = null;
			boolean found = false;
			// System.out.println("Left name "+left.name);
			// same variable occurred again, rename it
			if (vars.contains(var)) {
				found = true;
				previous = map.get(var);
				// Assume variables are of length 1
				// System.out.println("prev "+previous);
				lastVariable = (char) (lastVariable + 1);
				left.name = "" + lastVariable;
				// System.out.println("Replace " + left.name);
				map.put(var, left.name);
			} else {
				// add it for future conflict
				vars.add(var);
			}
			if (right != null)
				right.standarizeApart(map);

			// no left here as it is the variable name

			// backtrack
			if (found == true)
				if (previous != null)
					map.put(var, previous);
				else
					map.remove(var);

		} else {
			if (right != null)
				right.standarizeApart(map);
			if (left != null)
				left.standarizeApart(map);
		}
	}

	public void pushNegation(boolean negation) {

		if (type == PREDICATE) {
			if (negation)
				negate();
		} else if (type == NOT) {
			negation = !negation;
			// eliminate the node
			// get what is its position to the parent
			if (parent.left == this)
				parent.left = right;
			else
				parent.right = right;
			right.pushNegation(negation);
		} else if (type == OR || type == AND) {
			if (type == OR && negation)
				type = AND;
			else if (type == AND && negation)
				type = OR;
			if (left != null)
				left.pushNegation(negation);
			if (right != null)
				right.pushNegation(negation);
		} else if (type == EXIST || type == FORALL) {
			if (type == EXIST && negation)
				type = FORALL;
			else if (type == FORALL && negation)
				type = EXIST;
			if (right != null)
				right.pushNegation(negation);
			// There is no left as left is just the variable binding
		}

	}

	public void eliminateImplies() {
		if (type == IMPLIES) {
			type = OR;

			Node not = new Node(NOT);
			not.parent = this;
			not.right = left;
			left.parent = not;
			left = not;
		}
		if (left != null)
			left.eliminateImplies();
		if (right != null)
			right.eliminateImplies();
	}

	public Node clone() {
		Node leftClone = null, rightClone = null;
		if (left != null)
			leftClone = left.clone();
		if (right != null)
			rightClone = right.clone();
		Node res = new Node();
		res.type = type;
		res.isNegated = isNegated;
		res.name = name;
		for (String s : args)
			res.args.add(s);
		res.left = leftClone;
		res.right = rightClone;
		return res;
	}
}
